/*
 * SATSolver.cuh
 *
 *  Created on: Jul 25, 2013
 *      Author: jaime
 */

#include "SATSolver.cuh"

__device__ SATSolver::SATSolver(CUDAClauseVec &formula, int number_of_variables,
		int max_implication_per_var, GPUVec<Var> & dead_variables,
#ifdef ENABLE_STATISTICS
		RuntimeStatistics * statistics,
#endif
		NodesRepository<GPULinkedList<WatchedClause*>::Node > * node_repository
		//,GPUVec<WatchedClause> & watched_clauses
		)
:
  variables_handler(number_of_variables, dead_variables, &decision_maker),
  conflictAnalyzer(number_of_variables,
		  &formula, &variables_handler,
#if CONFLICT_ANALYSIS_STRATEGY != FULL_SPACE_SEARCH
#ifdef USE_CONFLICT_ANALYSIS
		  true,
#else
		  false,
#endif
#endif
		  max_implication_per_var, &decision_maker
#ifdef ENABLE_STATISTICS
		  ,statistics
#endif
#if CONFLICT_ANALYSIS_STRATEGY == TWO_WATCHED_LITERALS
		  ,node_repository
		  //, watched_clauses
#endif

		  )
,
		  decision_maker(&variables_handler, formula, number_of_variables)
#ifdef  USE_RESTART
		, geometric_restart(GEOMETRIC_CONFLICTS_BEFORE_RESTART, GEOMETRIC_RESTART_INCREASE_FACTOR)
#endif
{
#ifdef USE_RESTART
#endif

	this->formula = &formula;
	//this->decision_level = 0;
	this->number_of_variables = number_of_variables;
	this->current_status = UNDEF;
	next_decision.decision_level = NULL_DECISION_LEVEL;
#ifdef ENABLE_STATISTICS
	this->stats = statistics;
#endif

}

__device__ void SATSolver::restart()
{

#ifdef USE_RESTART
	conflictAnalyzer.restart();
#endif

}

/**
 * Solve with no assumptions.
 */
__device__ sat_status SATSolver::solve()
{
#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
	GPUVec<Lit> no_assumptions(0);
#else
	GPUStaticVec<Lit> no_assumptions;
#endif
	sat_status status = solve(&no_assumptions);

	variables_handler.set_assumptions(NULL);

	return status;
}

/**
 * Solve using assumptions.
 */
__device__ sat_status SATSolver::solve(
#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
		GPUVec<Lit> * assumptions
#else
		GPUStaticVec<Lit> * assumptions
#endif
		)
{



#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("Block %d, thread %d is starting to solve...\n", blockIdx.x, threadIdx.x);
	}
#endif
#ifdef ENABLE_STATISTICS
	stats->signal_preprocess_start();
#endif
	sat_status status_post_assumptions = preprocess(assumptions);
#ifdef ENABLE_STATISTICS
	stats->signal_preprocess_stop();
#endif

	if(status_post_assumptions == SAT)
	{
#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
		{
			printf("SAT on pre-processing!\n");
			variables_handler.print_assumptions();
			variables_handler.print_decisions();
			variables_handler.print_implications();
		}
#endif
		current_status = SAT;
		return SAT;
	}
	if(status_post_assumptions == UNSAT)
	{
#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
		{
			variables_handler.print_assumptions();
			variables_handler.print_decisions();
			variables_handler.print_implications();
			printf("UNSAT on pre-processing!\n");
		}
#endif
		current_status = UNSAT;
		return UNSAT;
	}

	sat_status status;

	int number_of_iterations = 0;

#ifdef USE_ASSERTIONS
	assert(!variables_handler.no_free_variables());
#endif

#ifdef IMPLICATION_GRAPH_DEBUG
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("DEBUG (%d, %d): starting loop.\n", blockIdx.x, threadIdx.x);
	}
#endif


	while(true)
	{

#if defined(IMPLICATION_GRAPH_DEBUG) || defined(DEBUG_THROUGH_VARIABLES_STATUS)
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("DEBUG (%d, %d): implication graph on iteration %d is:\n", blockIdx.x, threadIdx.x, number_of_iterations);
		//conflictAnalyzer.print_graph();
		variables_handler.print_decisions();
		variables_handler.print_implications();
		variables_handler.print_assumptions();
	}
#endif
#ifdef ENABLE_STATISTICS
		stats->signal_decision_start();
#endif
		bool decision_status =
				decision_maker.decide().decision_level != NULL_DECISION_LEVEL;//decide();
#ifdef ENABLE_STATISTICS
		stats->signal_decision_stop();
#endif
#ifdef DEBUG
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
		{
			printf("(after decision) ");
			variables_handler.print_decisions();
			variables_handler.print_assumptions();
		}
#endif
		if(!decision_status)
		{
			status = UNSAT;
#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
			if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
			{
				printf("Decision maker returned false!\n");
			}
#endif

			break;
		}
#ifdef ENABLE_STATISTICS
		stats->signal_conflict_analysis_start(variables_handler.get_decision_level());
#endif
		status = propagate(variables_handler.get_last_decision());
#ifdef ENABLE_STATISTICS
		stats->signal_conflict_analysis_stop(variables_handler.get_decision_level());
#endif

#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
			if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
			{
				printf("Propagate returned status:");
				print_status(status);
				printf("\n");
			}
#endif

		if(status != UNDEF)
			break;


		if(variables_handler.no_free_variables())
		{
			status = SAT;
			break;
		}

#ifdef USE_RESTART

		for(int i= 0; i < conflictAnalyzer.get_number_last_conflicts(); i++)
			geometric_restart.signal_conflict();

		if(geometric_restart.should_restart())
		{
			restart();
		}
#endif

		number_of_iterations++;

#ifdef MAX_ITERATIONS
		if(number_of_iterations > MAX_ITERATIONS)
		{
			printf("Limit of iterations has been reached. No answer was found.\n");
			current_status = UNDEF;
			return UNDEF;
		}
#endif

	}

#ifdef DEBUG_THROUGH_VARIABLES_STATUS
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("Solved: ");
		print_status(status);
		printf("\n");
		variables_handler.print_all();
	}
#endif

	if(status == SAT)
	{
#ifdef DEBUG
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
			printf("It seems that the formula is SAT!\n");
#endif
		current_status = SAT;
	}

	if(status == UNSAT || status == UNDEF)
	{
#ifdef DEBUG
		if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
			printf("The formula seems to be UNSAT!\n");
#endif
		current_status = UNSAT;
	}

#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
		printf("Solving is done.\n");
#endif

	return current_status;

}

/**
 * Propagates the currents decisions and implications, possibly generating more
 * implications (BCP through UP). Returns if the decisions have satisfied, unsatisfied or not
 * changed the current status of the formula.
 */
__device__ sat_status SATSolver::propagate(Decision d)
{
	return conflictAnalyzer.propagate(d);
}


/**
 * This method sets the assumptions, remove the assumptions from the free variables and
 * propagate the assumptions.
 */
__device__ sat_status SATSolver::preprocess(
#ifdef ASSUMPTIONS_USE_DYNAMICALLY_ALLOCATED_VECTOR
		GPUVec<Lit> * assumptions
#else
		GPUStaticVec<Lit> * assumptions
#endif

)
{
	stats->signal_pre_proc_handling_variables_start();
	variables_handler.set_assumptions(assumptions);
	stats->signal_pre_proc_handling_variables_stop();
	sat_status status_post_preprocessing =
			conflictAnalyzer.set_assumptions(assumptions);

	//variables_handler.print_assumptions();

	if(status_post_preprocessing != UNDEF)
	{
		return status_post_preprocessing;
	}

#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		printf("Starting to pre-process. Assumptions:\n");
		variables_handler.print_assumptions();
	}
#endif


	if(variables_handler.no_assumptions()
			&& variables_handler.no_implications()
			&&	variables_handler.no_decisions())
		return UNDEF;

	if(status_post_preprocessing == UNDEF &&
			variables_handler.no_free_variables())
	{
		status_post_preprocessing = SAT;
	}

#if defined(DEBUG) || defined(IMPLICATION_GRAPH_DEBUG)
	if(DEBUG_SHOULD_PRINT(threadIdx.x, blockIdx.x))
	{
		//printf("Preprocessing has generated this implication graph:\n");
		//conflictAnalyzer.print_graph();
	}
#endif

	return status_post_preprocessing;

}

__device__ void SATSolver::get_results(Lit* results)
{


	if(current_status != SAT)
	{
		return;
	}
	else
	{

		int next_pos = 0;

		for(int i = 0; i < variables_handler.number_of_decisions(); i++)
		{

			results[next_pos] = variables_handler.get_decision(i).literal;
			next_pos++;

		}

		if(variables_handler.assumptions_set())
		{
			for(int i = 0; i < variables_handler.number_of_assumptions(); i++)
			{

				results[next_pos] = variables_handler.get_assumption(i);
				next_pos++;
			}
		}
		for(int i = 0; i < variables_handler.number_of_implications(); i++)
		{

			results[next_pos] = variables_handler.get_implication(i).literal;
			next_pos++;
		}



	}

}

__device__ int SATSolver::get_results_size()
{
	int size =  variables_handler.number_of_decisions()
			+variables_handler.number_of_implications();

	size += variables_handler.assumptions_set() ? variables_handler.number_of_assumptions() : 0;
	return size;

}

/**
 * Resets the SAT Solver, allowing to used it again.
 * Does not delete the learnt clauses (when implemented).
 */
__device__ void SATSolver::reset()
{

	variables_handler.reset();

	current_status = UNDEF;

	conflictAnalyzer.reset();



}

__device__ void SATSolver::print_structures()
{
	conflictAnalyzer.print_graph();
	variables_handler.print_assumptions();
	variables_handler.print_decisions();
	variables_handler.print_implications();
}

